Process Analysis Toolkit (PAT) 3.5 Help |
Sites for Verification Global Variable As Orc does not have a notion of global variable, in order to be able to
easily assert a global property that holds throughout the program, we extend Orc
with a notion of global variable. Global variable in Orc must prefixed
by globalvar keyword, and defining at the beginning of the
program. GUpdate Site To assign a value to a global variable directly, a special site
$GUpdate is provided. Consider the metronome example in Section 3.8.1.1 with
global variables and $GUpdate inserted, globalvar tickNum = 0 we can verify whether it is possible to have two consecutive "tick"s or two
consecutive "tock"s by checking whether the system is able to reach the state
satisfying (tickNum < 0 \/ tickNum > 1). Global Variable InitializationSometimes, global variable
need to be initialized before its use. The intialization section is
declared just after the global variable declaration, and the section
is surrounded by curly bracket { }. Consider the example below, the global variable arr is a two-element array,
and it is initialize with the value [2,1] before it is passed the the quicksort
function. globalvar arr=Array(2) External Sites Modeling Service orchestration systems would normally involve external services.
External services would incur, furthermore, there might be cases where
communication halted unexpectedly, or the services simply non-responsive. Following is the syntax that used to model the external site, ExternalSite
SiteName(Args)[haltAllow{Delay}]{DelayTups} where ExternalSite and EndSite denotes the start and end of the external site
modeling. SiteName is the service name of the external site; Args is a set of
arguments for the site; haltAllow is an optional tag to specify whether to model
the halting behavior, and Delays is a set of natural numbers which denotes the
possible delays before halting. DelayTups is a set of tuple (t1,t2) which is
used to specify all possible communication delays of the external service. The
domain of t1 and t2 is natural numbers. t1 is the forward trip delay, which is
used to specify the communication delay for the service call to reach the
external services plus the processing time needed just before the internal
storage of external services is updated. For simplicity of modeling, internal
storage of external services are assumed to be updated instantaneously at time
t1 and if there are multiple internal storages to be updated, we assumed all are
updated at the same time. t2 is the return trip delay, which is used to specify
the processing time of the external services just after the update of internal
storage plus the delay of returned value traveling back from the external
service. Thus, the total roundtrip delay is t1 + t2. DelayTups also allows a
special "inf "(infinity delay) symbol, which is used to denote the
non-responsive behavior. SystemVarDecl is a list of system variable
declarations, which is used to model the global internal storage for the
stateful external service. All the system variable declarations are required to
start with the systemvar keyword. SystemVarInits is the section that initialize
the declared system variables, and the section is surrounded by curly
bracket {} just like global variable intialization.ORCExpression is the body of
the external site modelling and it is used to specify the output value of
external site with respect to the input arguments Args. Example - Auction Service ExternalSite Auction(x)[haltAllow{1, 2}]{(1,1), inf}
= The above syntax specifies an Auction external site. AuctionList
is started with a value "1".
metronome(1000) >> $GUpdate({tickNum = tickNum +
1})>>
"tick"
| Rtimer(500) >> metronome(1000)
>> $GUpdate({tickNum = tickNum - 1})
>> "tock"
{arr.set(0,2)>>arr.set(1,1)}
def quicksort{a}= ...
quicksort(arr)
SystemVarDecls
{SystemVarInits}
ORCExpression
EndSite
systemvar AuctionList = Buffer()
{AuctionList.put("1")}
(x > ("post", item) >
AuctionList.put(item)
|
x >
"getNext" > AuctionList.getnb()
EndSite
Assume argument x=("post", 100), the
possible behaviors are